es:ES, l:IdLnk, tg:Id, A:Type.
(e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (es-in-port(es;l;tg)
 (=
 (es-triggers(es;destination(l);;es-in-port-conds(A;l;tg))
 ( AbsInterface(A)) 

latex

Definitions

ES, t  T, IdLnk, Id, Type, x:A. B(x), valtype(e), rcv(l,tg), kind(e), Knd, s = t, x:AB(x), P  Q, E, es-in-port(es;l;tg), <a, b>, AbsInterface(A), x  dom(f), x : v, es-triggers(es;i;ds;conds), es-in-port-conds(A;l;tg), EqDecider(T), Unit, left + right, x:A  B(x), EOrderAxioms(E; pred?; info), f(a), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , b, constant_function(f;A;B), P & Q, Top, let x,y = A in B(x;y), Atom$n, t.1, False, A, True, ff, A c B, Void, if b then t else f fi , val(e), P  Q, {T}, SQType(T), s ~ t, , case b of inl(x) => s(x) | inr(y) => t(y), tag(e), lnk(e), isrcv(e), inl x , b, P  Q, tt, p  q, P  Q, T, x.A(x), inr x , destination(l), loc(e), a = b, a = b, p q, x:A.B(x), , source(l)

Lemmas

or functionality wrt iff, es-isrcv-loc, Knd sq, es-kind-rcv, lsrc wf, es-loc-pred, es-loc-rcv, assert-eq-knd, top wf, it wf, bor wf, eq knd wf, eq id wf, es-loc wf, ldst wf, assert of bor, false wf, squash wf, bool wf, bnot thru bor, assert of band, and functionality wrt iff, band wf, btrue wf, true wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bnot wf, not wf, assert wf, bfalse wf, es-rcv-kind, Id sq, es-val wf, es-E wf, Knd wf, es-kind wf, rcv wf, es-valtype wf, Id wf, IdLnk wf, event system wf